\begin{tabbing}
gcd\_p($a$; $b$; $y$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=divides($y$; $a$)\+
\\[0ex]$\wedge$ divides($y$; $b$)
\\[0ex]$\wedge$ ($\forall$$z$:$\mathbb{Z}$. (divides($z$; $a$) $\wedge$ divides($z$; $b$)) $\Rightarrow$ divides($z$; $y$))
\-
\end{tabbing}